\begin{tabbing}
ecl{-}mng{-}update\=\{i:l\}\+
\\[0ex](${\it es}$; $i$; ${\it ds}$; ${\it da}$; $x$; $z$; ${\it upd}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)\+
\\[0ex]$\Rightarrow$ alle{-}at(${\it es}$;$i$;$e$.\=es{-}after(${\it es}$; $z$; $e$)\+
\\[0ex]$=$
\\[0ex]list\_accum(\=${\it z'}$,${\it nf}$.\=${\it nf}$/$n$,$f$.\+\+
\\[0ex]if \=es{-}bact\=\{i:l\}\+\+
\\[0ex](${\it ds}$; ${\it da}$; $x$; ${\it es}$; $n$; es{-}init(${\it es}$;$e$); $e$)$\rightarrow$
\-\\[0ex]$f$(es{-}state{-}when(${\it es}$;$e$),es{-}val(${\it es}$; $e$))
\-\\[0ex]else ${\it z'}$ fi;
\-\\[0ex]es{-}when(${\it es}$; $z$; $e$);
\\[0ex]fpf{-}cap(${\it upd}$;product{-}deq(Knd;Id;KindDeq;IdDeq);\=$\langle$\=es{-}kind\+\+
\\[0ex](${\it es}$; $e$)
\-\\[0ex]$,\,$$z$$\rangle$;nil))
\-\-\\[0ex]$\in$ fpf{-}cap(${\it ds}$;IdDeq;$z$;Top))
\-\-
\end{tabbing}